(0) Obligation:
The Runtime Complexity (innermost) of the given
CpxTRS could be proven to be
BOUNDS(1, n^1).
The TRS R consists of the following rules:
++(nil, y) → y
++(x, nil) → x
++(.(x, y), z) → .(x, ++(y, z))
++(++(x, y), z) → ++(x, ++(y, z))
Rewrite Strategy: INNERMOST
(1) NestedDefinedSymbolProof (BOTH BOUNDS(ID, ID) transformation)
The TRS does not nest defined symbols.
Hence, the left-hand sides of the following rules are not basic-reachable and can be removed:
++(++(x, y), z) → ++(x, ++(y, z))
(2) Obligation:
The Runtime Complexity (innermost) of the given
CpxTRS could be proven to be
BOUNDS(1, n^1).
The TRS R consists of the following rules:
++(.(x, y), z) → .(x, ++(y, z))
++(nil, y) → y
++(x, nil) → x
Rewrite Strategy: INNERMOST
(3) TrsToWeightedTrsProof (BOTH BOUNDS(ID, ID) transformation)
Transformed TRS to weighted TRS
(4) Obligation:
The Runtime Complexity (innermost) of the given
CpxWeightedTrs could be proven to be
BOUNDS(1, n^1).
The TRS R consists of the following rules:
++(.(x, y), z) → .(x, ++(y, z)) [1]
++(nil, y) → y [1]
++(x, nil) → x [1]
Rewrite Strategy: INNERMOST
(5) TypeInferenceProof (BOTH BOUNDS(ID, ID) transformation)
Infered types.
(6) Obligation:
Runtime Complexity Weighted TRS with Types.
The TRS R consists of the following rules:
++(.(x, y), z) → .(x, ++(y, z)) [1]
++(nil, y) → y [1]
++(x, nil) → x [1]
The TRS has the following type information:
++ :: .:nil → .:nil → .:nil
. :: a → .:nil → .:nil
nil :: .:nil
|
Rewrite Strategy: INNERMOST
(7) CompletionProof (UPPER BOUND(ID) transformation)
The transformation into a RNTS is sound, since:
(a) The obligation is a constructor system where every type has a constant constructor,
(b) The following defined symbols do not have to be completely defined, as they can never occur inside other defined symbols:
++
(c) The following functions are completely defined:
none
Due to the following rules being added:
none
And the following fresh constants:
const
(8) Obligation:
Runtime Complexity Weighted TRS where critical functions are completely defined. The underlying TRS is:
Runtime Complexity Weighted TRS with Types.
The TRS R consists of the following rules:
++(.(x, y), z) → .(x, ++(y, z)) [1]
++(nil, y) → y [1]
++(x, nil) → x [1]
The TRS has the following type information:
++ :: .:nil → .:nil → .:nil
. :: a → .:nil → .:nil
nil :: .:nil
const :: a
|
Rewrite Strategy: INNERMOST |
(9) NarrowingProof (BOTH BOUNDS(ID, ID) transformation)
Narrowed the inner basic terms of all right-hand sides by a single narrowing step.
(10) Obligation:
Runtime Complexity Weighted TRS where critical functions are completely defined. The underlying TRS is:
Runtime Complexity Weighted TRS with Types.
The TRS R consists of the following rules:
++(.(x, y), z) → .(x, ++(y, z)) [1]
++(nil, y) → y [1]
++(x, nil) → x [1]
The TRS has the following type information:
++ :: .:nil → .:nil → .:nil
. :: a → .:nil → .:nil
nil :: .:nil
const :: a
|
Rewrite Strategy: INNERMOST |
(11) CpxTypedWeightedTrsToRntsProof (UPPER BOUND(ID) transformation)
Transformed the TRS into an over-approximating RNTS by (improved) Size Abstraction.
The constant constructors are abstracted as follows:
nil => 0
const => 0
(12) Obligation:
Complexity RNTS consisting of the following rules:
++(z', z'') -{ 1 }→ x :|: z'' = 0, z' = x, x >= 0
++(z', z'') -{ 1 }→ y :|: z'' = y, y >= 0, z' = 0
++(z', z'') -{ 1 }→ 1 + x + ++(y, z) :|: z'' = z, z >= 0, z' = 1 + x + y, x >= 0, y >= 0
(13) SimplificationProof (BOTH BOUNDS(ID, ID) transformation)
Simplified the RNTS by moving equalities from the constraints into the right-hand sides.
(14) Obligation:
Complexity RNTS consisting of the following rules:
++(z', z'') -{ 1 }→ z' :|: z'' = 0, z' >= 0
++(z', z'') -{ 1 }→ z'' :|: z'' >= 0, z' = 0
++(z', z'') -{ 1 }→ 1 + x + ++(y, z'') :|: z'' >= 0, z' = 1 + x + y, x >= 0, y >= 0
(15) CpxRntsAnalysisOrderProof (BOTH BOUNDS(ID, ID) transformation)
Found the following analysis order by SCC decomposition:
(16) Obligation:
Complexity RNTS consisting of the following rules:
++(z', z'') -{ 1 }→ z' :|: z'' = 0, z' >= 0
++(z', z'') -{ 1 }→ z'' :|: z'' >= 0, z' = 0
++(z', z'') -{ 1 }→ 1 + x + ++(y, z'') :|: z'' >= 0, z' = 1 + x + y, x >= 0, y >= 0
Function symbols to be analyzed: {
++}
(17) IntTrsBoundProof (UPPER BOUND(ID) transformation)
Computed SIZE bound using CoFloCo for: ++
after applying outer abstraction to obtain an ITS,
resulting in: O(n1) with polynomial bound: z' + z''
(18) Obligation:
Complexity RNTS consisting of the following rules:
++(z', z'') -{ 1 }→ z' :|: z'' = 0, z' >= 0
++(z', z'') -{ 1 }→ z'' :|: z'' >= 0, z' = 0
++(z', z'') -{ 1 }→ 1 + x + ++(y, z'') :|: z'' >= 0, z' = 1 + x + y, x >= 0, y >= 0
Function symbols to be analyzed: {
++}
Previous analysis results are:
++: runtime: ?, size: O(n1) [z' + z'']
|
(19) IntTrsBoundProof (UPPER BOUND(ID) transformation)
Computed RUNTIME bound using CoFloCo for: ++
after applying outer abstraction to obtain an ITS,
resulting in: O(n1) with polynomial bound: 1 + z'
(20) Obligation:
Complexity RNTS consisting of the following rules:
++(z', z'') -{ 1 }→ z' :|: z'' = 0, z' >= 0
++(z', z'') -{ 1 }→ z'' :|: z'' >= 0, z' = 0
++(z', z'') -{ 1 }→ 1 + x + ++(y, z'') :|: z'' >= 0, z' = 1 + x + y, x >= 0, y >= 0
Function symbols to be analyzed:
Previous analysis results are:
++: runtime: O(n1) [1 + z'], size: O(n1) [z' + z'']
|
(21) FinalProof (EQUIVALENT transformation)
Computed overall runtime complexity
(22) BOUNDS(1, n^1)